(0) Obligation:
The Runtime Complexity (innermost) of the given
CpxTRS could be proven to be
BOUNDS(1, n^1).
The TRS R consists of the following rules:
active(zeros) → mark(cons(0, zeros))
active(tail(cons(X, XS))) → mark(XS)
active(cons(X1, X2)) → cons(active(X1), X2)
active(tail(X)) → tail(active(X))
cons(mark(X1), X2) → mark(cons(X1, X2))
tail(mark(X)) → mark(tail(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(tail(X)) → tail(proper(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
tail(ok(X)) → ok(tail(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
Rewrite Strategy: INNERMOST
(1) NestedDefinedSymbolProof (BOTH BOUNDS(ID, ID) transformation)
The following defined symbols can occur below the 0th argument of cons: active, proper, cons
The following defined symbols can occur below the 1th argument of cons: active, proper, cons
The following defined symbols can occur below the 0th argument of top: active, proper, cons
The following defined symbols can occur below the 0th argument of proper: active, proper, cons
The following defined symbols can occur below the 0th argument of active: active, proper, cons
Hence, the left-hand sides of the following rules are not basic-reachable and can be removed:
active(tail(cons(X, XS))) → mark(XS)
active(tail(X)) → tail(active(X))
proper(tail(X)) → tail(proper(X))
(2) Obligation:
The Runtime Complexity (innermost) of the given
CpxTRS could be proven to be
BOUNDS(1, n^1).
The TRS R consists of the following rules:
top(ok(X)) → top(active(X))
tail(mark(X)) → mark(tail(X))
proper(zeros) → ok(zeros)
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
proper(0) → ok(0)
tail(ok(X)) → ok(tail(X))
active(zeros) → mark(cons(0, zeros))
cons(mark(X1), X2) → mark(cons(X1, X2))
top(mark(X)) → top(proper(X))
active(cons(X1, X2)) → cons(active(X1), X2)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
Rewrite Strategy: INNERMOST
(3) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)
A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 5.
The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by:
final states : [1, 2, 3, 4, 5]
transitions:
ok0(0) → 0
mark0(0) → 0
zeros0() → 0
00() → 0
top0(0) → 1
tail0(0) → 2
proper0(0) → 3
cons0(0, 0) → 4
active0(0) → 5
active1(0) → 6
top1(6) → 1
tail1(0) → 7
mark1(7) → 2
zeros1() → 8
ok1(8) → 3
cons1(0, 0) → 9
ok1(9) → 4
01() → 10
ok1(10) → 3
tail1(0) → 11
ok1(11) → 2
01() → 13
zeros1() → 14
cons1(13, 14) → 12
mark1(12) → 5
cons1(0, 0) → 15
mark1(15) → 4
proper1(0) → 16
top1(16) → 1
mark1(7) → 7
mark1(7) → 11
ok1(8) → 16
ok1(9) → 9
ok1(9) → 15
ok1(10) → 16
ok1(11) → 7
ok1(11) → 11
mark1(12) → 6
mark1(15) → 9
mark1(15) → 15
active2(8) → 17
top2(17) → 1
active2(10) → 17
proper2(12) → 18
top2(18) → 1
02() → 20
zeros2() → 21
cons2(20, 21) → 19
mark2(19) → 17
proper2(13) → 22
proper2(14) → 23
cons2(22, 23) → 18
zeros2() → 24
ok2(24) → 23
02() → 25
ok2(25) → 22
proper3(19) → 26
top3(26) → 1
cons3(25, 24) → 27
ok3(27) → 18
proper3(20) → 28
proper3(21) → 29
cons3(28, 29) → 26
zeros3() → 30
ok3(30) → 29
03() → 31
ok3(31) → 28
active3(27) → 32
top3(32) → 1
cons4(31, 30) → 33
ok4(33) → 26
active4(25) → 34
cons4(34, 24) → 32
active4(33) → 35
top4(35) → 1
active5(31) → 36
cons5(36, 30) → 35
(4) BOUNDS(1, n^1)